es-sends-iff2(es;l;tg;B;ds;e.P(e);e.f(e))
== ((e:E. (kind(e) = rcv(l,tg))  (valtype(e) r B)) & (x:Id. vartype(source(l);x) r ds(x)?Top))
== c (e@source(l). P(e)  (e':E. ((kind(e') = rcv(l,tg)) c (sender(e') = e)))
== c & (e':E. (kind(e') = rcv(l,tg))  (P(sender(e')) c (val(e') = f(sender(e')))))
== c & (e':E.
== c & ((kind(e') = rcv(l,tg))
== c & ( (e'':E.
== c & ( (isrcv(e''))  (lnk(e'') = l)  (sender(e'') = sender(e'))  (e'' = e')))) 

latex

---

clarification:

es-sends-iff2(es;l;tg;B;ds;e.P(e);e.f(e))
== ((e:es-E(es). (es-kind(es; e) = rcv(l,tg)  Knd)  (es-valtype(es; e) r B))
== & (x:Id. es-vartype(es; source(l); x) r fpf-cap(ds;IdDeq;x;Top)))
== c (alle-at(es;source(l);e.P(e)
== c  (e':es-E(es)
== c  (((es-kind(es; e') = rcv(l,tg)  Knd) c (es-sender(es; e') = e  es-E(es)))))
== c & (e':es-E(es).
== c & ((es-kind(es; e') = rcv(l,tg)  Knd)
== c & ( (P(es-sender(es; e')) c (es-val(es; e') = f(es-sender(es; e'))  B)))
== c & (e':es-E(es).
== c & ((es-kind(es; e') = rcv(l,tg)  Knd)
== c & ( (e'':es-E(es).
== c & ( (es-isrcv(es; e''))
== c & (  (es-lnk(es; e'') = l  IdLnk)
== c & (  (es-sender(es; e'') = es-sender(es; e')  es-E(es))
== c & (  (e'' = e'  es-E(es))))) 

latex

Definitions	valtype(e), Id, vartype(i;x), f(x)?z, IdDeq, Top, e@i. P(e), source(l), x:A. B(x), P & Q, A c B, val(e), Knd, kind(e), rcv(l,tg), x:A. B(x), b, isrcv(e), IdLnk, lnk(e), P  Q, sender(e), s = t, E
FDL editor aliases	es-sends-iff2